.cent(Practical Termination for Nondeterministic Programs)
 
Traditionally, the word "termination" has a very well understood
meaning, namely "it stops".  However, one might consider several different
kinds of termination.  For example, when we speak of nondeterministic
languages, such as logic, there are at least 3 different ways of considering
the question of termination.

The "safe" interpretation of termination in the presence of nondeterminism
is to say: a program always "terminates" if and only if every possible
computation path terminates. This is the most common interpretation, but
it may be more restrictive than necessary.
 
At the other extreme we could say the program "terminates" if there exists a
computation path which terminates.  This interpretation is sufficient if we can
always find the appropriate path for each computation.  
 
A third interpretation is one in which
we say that a program always terminates with respect to a particular interpreter,
or a particular evaluation strategy.  We all know that there are programs
which will terminate under call-by-name evaluation and not under call-by-value
(in the presence of side effects, the reverse is also true).
If we use a breadth first search, or computation strategy, (that is, follow
all paths in parallel)
we know that we will 
always be able to discover a terminating computation if any exists.
However, this can be extremely costly in both time and space, and is not
usually necessary.  Using
the "safe" definition of termination, the computation rule used makes no
difference; however, we restrict ourselves unnecessarily from considering
programs which will always terminate under the conditions in which
we intend to use them.

We intend to consider termination in a pragmatic way.  Our treatment is informal
and intended to make some useful special cases obvious to the novice who finds
the subject of proving termination of programs prohibitively complicated at 
first glance and is thus discouraged from the endeavor entirely.
We shall describe a useful class of programs, guaranteed to terminate given
certain restrictions on the calling style.  Since we will be dealing with
logic programs (partially correct by definition), we will have totally 
correct programs.

A logic program is a set of Horn clauses, each of which is an implication with
at most one consequent.  For example,
.begin center
%dA ← B%41%d ∧ B%42%d ∧ ... ∧ B%4n%1
.end

The procedural interpretation of a Horn clause is as a procedure declaration
[Kowalski, 1973].  The consequent, %dA%1, is the procedure name and the list of
subgoals %dB%41%d, ..., B%4n%1 make up the procedure body.  A clause with an empty
list of subgoals is thus a procedure with no body and is taken to be an assertion
 of fact.
A clause in which the procedure name is missing, for example
.begin center
%d← B%41%d ∧ ... ∧ B%4n%1
.end

is taken to be a nameless procedure or simply a sequence of goals to be satisfied.

A logic program is an assertional specification of the relationships which hold
among the objects it operates on.  It is a statement of its own axiomatic semantics.
However, we do not wish to consider here all syntactically correct logic programs,
but only those which are "computational",
that is, programs whose computation is well spelled out.  For example,
a program may be driven by the structure of the data it operates on,
decomposing that structure until a basis case is reached.

This of course requires that we know which of the arguments to a predicate
are intended to provide input, the computation being based on the 
decomposition of one or more of these arguments to a basis case or perhaps,
as in the case
of real number algorithms, based on reaching some acceptable error tolerance.

Given the restriction that we will always specify which of the arguments
are intended to be input and which are intended to hold the answer, we
consider termination with respect to these conventions.
   For example, a logic program which computes the greatest common divisor
of two given natural numbers is as follows:
.begin select d
.nofill

	GCD(0,x,x) ←
.group skip 1
	GCD(x,0,x) ←
.group skip 1
	GCD(x,y,z) ← %1≤%d(x,y) ∧ GCD(x,y-x,z) ∧ Nat(x) ∧ Nat(y-x)
.group skip 1
 
	GCD(x,y,z) ← %1≤%d(y,x) ∧ GCD(x-y,y,z) ∧ Nat(x-y) ∧ Nat(y)
.group skip 1
 
GCD(x,y,z) %1means that the greatest common divisor of%d x %1and %dy %1is%d z.
%1≤%d(x,y)%1 means that %dx%1 is less than or equal to %dy.
Nat(x) %1means that %dx%1 is a natural number.
.group skip 1
.end
 
The logic program %dGCD%1 is easily shown to terminate as long as we always
provide the natural numbers %dx%1 and %dy%1 as input and expect to compute their
greatest common divisor in %dz%1.  If however, we were to provide natural numbers
 for %dx%1 and %dz%1,
asking in effect for %dy%1, a number such that the %dGCD(x,y,z)%1, the program
may never terminate.  If %dz%1 does not divide %dx%1 then we can never find an answer,
and if %dz%1 does divide %dx%1, then there are an infinite number of answers.  Thus,
if we are to compute all of them, we will never terminate.
Furthermore, if we are content to stop at one answer, it may be a different one
every time the program is run, since
we have no indication in the program of how to generate possible
%dy%1 values.  Without knowing the internal workings of the interpreter we can't
tell how this may be done.  Thus, the %dGCD%1 program is considered "computational"
only given the restriction that x and y are to be input values and z an output
value.

  This approach does not profit from the generality of logic programs, which
express relationships among arguments rather than simply supply output.
However, we contend that most
programs are written with the intent of providing answers which are 
functions of some input.  We usually know which information is going
to be available and which is to be computed.⊗↓The notable exception to this
generalization is data base handling.  Logic programs are naturals
for this kind of application, expressing relationships among elements of
the data base and being capable of retrieving information on any of the missing
arguments.  See [van Emden] for this type application.←
We base our algorithms on this knowledge.  When
we are computing a function of some arguments we know that there is exactly
one answer.  However, a well-defined function may map several different
sets of arguments in its domain to the same value in its range, destroying the
functionality of the inverse operation, as in the example above.
 
We consider computational logic programs to be those in which
the computation is driven in such a way as to
simplify each recursive call in the sense of getting closer to the basis
or termination clauses of the program.  Not only does this simplification
have to happen but it has to happen "fast enough".  That is, we must be
convinced that we cannot have an infinite chain of simplifications
between the case at hand and the basis case.
     This causes no trouble if we are using inductively defined data
structures, since there is always a finite number of applications of
constructors to basis elements which make up any element of the data
structure.  However, in the case of real number algorithms, we have the
additional problem of showing that we reduce the problem fast enough to
reach our tolerance of error. See [Clark, McKeeman, Sickel, 1978].  Here
we simplify matters by considering only programs which operate on
inductively definable domains.

For logic programs which are computational in the sense described above we
can speak of termination in a pragmatic way.  We specify which parameters 
are to be input and which are to be output, and guarantee termination only
under these restrictions.

The decomposition of the input values in a computational logic program need 
not be an explicit stripping of constructor functions.  For example, in the
%dGCD%1 program, we do not intend to represent every natural number as a
sequence of applications of "successor" to "0".  We include as a subgoal
the resrtriction that we are at each step stil dealing with natural numbers.
This allows us to use the built in data types of the machine we are using
and to define others in terms of them.  For example, if a type "integer" is
available, it is more convenient to define %dNat(x)%1,"%dx%1 is a natural
number", as "%dx%1 is an integer grater than or equal to 0", and be able to
use built in integer arithmetic, rather than define natural numbers inductively
from 0 and successor and redefine all arithmetic functions to operate on them
appropriately.

.begin nofill
.fp
Theorem

.end
.fp
Let %dP%1 be a recursive program which operates on an inductively defined
data structure %dD%1 (one for which it is possible to give an inductive
definition). Let %dx%1 be a formal parameter to %dP%1.  Then, %dP%1 will terminate
if
.begin nofill
	1)  The termination, or basis, clause of %dP%1 is applicable if %dx%1 is 
bound to any basis element of %dD%1; and
	2)  The value of %dx%1 is simplified, or decomposed, with every
recursive call to the program; and
	3)  There are no non-terminating subgoals.
.pt24
.end
.fp
proof:  by induction on the number of applications of the constructor function
involved in the value of %dx%1.  Since by 2) %dx%1 is decomposed in every
recursive call, the only applicable clause will be a termination clause when %dx%1
is a basis element. (i.e. it will be impossible to further decompose %dx%1 so
no recursive call will be applicable)

.pt24
The third condition of the theorem implies that we are building up definitions
of programs from others which are known to terminate.  It is reasonable to
assume we are given certain primitive programs which are guaranteed to terminate
with which to build more complex programs.  We wish to have confidence that we
can combine correct components is such a way as to guarantee correctness.
One can ensure proper termination for one's logic programs while making full
use of the tools at hand.  The rules to remember are:
.pt24
.fp
1) Specify which are input and which are output variables.
.pt24;fp
2) Insure that the termination case is all that is applicable when a basis
element of the data structure is operated on.
.pt24;fp
3) Each recursive call must simplify some designated input variable in the
sense of bringing it closer to the basis element(s) of the domain.
.pt24
The decomposition of the data structure must be done carefully when making use of
non-inductive definitions.  For example, in decomposing a natural number %dx%1,
we may simply subtract one, however, we must always be sure to check that the
result is indeed a natural number to ensure that we do not attempt to "decompose"
the basis element, "0".
 
When we have a specific purpose in mind it is reasonable to consider the properties
of our program when used only in the way intended.  It is also helpful to be able to 
%deasily%1 convince oneself of the correctness of a program intended to be used
the same way at all times.  It is this pragmatic view of termination which we've
taken in this paper with the hope of making at least some special cases obvious
to the novice who feels threatened by the formal theory and incapable of dealing with
the general case.
 
 
.cent(References)
.BEGIN  nofill
Clark, K., W. McKeeman, and S. Sickel, "Logic Programming Applied to 
	Numerical Integration", 1978.
 
Kowalski, R., "Predicate Logic as Programming Language", Memo no. 70,
	Edinburgh University, November, 1973.
 
van Emden, M. H., "Deductive Information Retrieval on Virtual Relational 
	Data Bases".
 
.end